T:Type, L, L1, L2:T List. interleaving(T;L1;L2;L)  {x:T. (x  L)  (x  L1)  (x  L2)} 

latex

Definitions	t  T, x:A. B(x), ||as||, ij, P  Q, False, A, AB, , disjoint_sublists(T;L1;L2;L), Prop, P & Q, (x  l), P  Q, P  Q, P  Q, {T}, interleaving(T;L1;L2;L), x:A. B(x), A & B, {i..j}, Inj(A; B; f), True, T, i  j < k, S  T, S  T, finite(T), SQType(T), Surj(A; B; f), Dec(P), l[i], L1  L2
Lemmas	member sublist, disjoint sublists sublist, select wf, decidable lt, le wf, int seg wf, nsub finite, disjoint sublists witness, l member wf, nat wf, disjoint sublists wf, non neg length, length wf1